/* 
 * $Id: SequenceNode.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright 2004
 *    Distributed Systems Research Group
 *    Department of Software Engineering
 *    Faculty of Mathematics and Physics
 *    Charles University, Prague
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 */

package org.objectweb.fractal.bpc.checker.node;

import java.util.ArrayList;
import java.util.TreeSet;

import org.objectweb.fractal.bpc.checker.DFSR.CheckingException;
import org.objectweb.fractal.bpc.checker.state.*;
import org.objectweb.fractal.bpc.checker.utils.AnotatedProtocol;

/**
 * This class Represents the sequence operator. It supports any finite number of
 * automata to be sequenced.
 */
public class SequenceNode extends TreeNode {

    /** Creates a new instance of SequenceNode */
    public SequenceNode(TreeNode[] nodes) {
        super(getProtocol(nodes));
        this.nodes = nodes;

        last = nodes.length - 1;
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getInitial()
     */
    public State getInitial() {
        if (initial == null) {
            State[] states = new State[nodes.length];
            for (int i = 0; i < nodes.length; ++i)
                states[i] = nodes[i].getInitial();

            initial = new IndexState(0, states);
        }

        return initial;
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#isAccepting(org.objectweb.fractal.bpc.checker.state.State)
     */
    public boolean isAccepting(State state) {
        IndexState istate = (IndexState) state;
        if ((istate.index == last)
                && (nodes[last].isAccepting(istate.states[istate.index])))
            return true;

        else if (nodes[istate.index].isAccepting(istate.states[istate.index])) {
            for (int i = istate.index + 1; i <= last; ++i) {
                if (!nodes[i].isAccepting(nodes[i].getInitial()))
                    return false;
            }
            
            return true;
        }

        else
            return false;
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getTransitions(org.objectweb.fractal.bpc.checker.state.State)
     */
    public TransitionPairs getTransitions(State state) throws InvalidParameterException, CheckingException {
        IndexState istate = (IndexState) state;
        int stindex = istate.index;

        if ((stindex != last)
                && (nodes[stindex].isAccepting(istate.states[stindex]))) {

            ArrayList tmptrans = new ArrayList();

            TransitionPair[] atrans = nodes[stindex].getTransitions(istate.states[stindex]).transitions;

            int tmpindex = stindex;
            int bsize = 0;
            do {
                ++tmpindex;

                TransitionPair[] btrans = nodes[tmpindex].getTransitions(nodes[tmpindex].getInitial()).transitions;

                tmptrans.add(btrans);

                bsize += btrans.length;

            } while ((nodes[tmpindex].isAccepting(nodes[tmpindex].getInitial()))
                    && (tmpindex < last));

            int alen = atrans.length;
            int blen = bsize;

            TransitionPair[] trans = new TransitionPair[alen + blen];

            for (int i = 0; i < alen; ++i) {
                State[] tmpstates = new State[istate.states.length];
                for (int k = 0; k < istate.states.length; ++k)
                    tmpstates[k] = istate.states[k];

                tmpstates[stindex] = atrans[i].state;

                trans[i] = new TransitionPair(atrans[i].eventIndex,
                        new IndexState(stindex, tmpstates));
            }

            int idx = alen;
            for (int j = 0; j < tmptrans.size(); ++j) {
                for (int i = 0; i < ((TransitionPair[]) tmptrans.get(j)).length; ++i, ++idx) {
                    State[] tmpstates = new State[istate.states.length];
                    for (int k = 0; k < istate.states.length; ++k)
                        // set the previous state to accepting if suitable
                        // this is only heuristics not influencing the correctness...
                        if ((k <= j) && (nodes[k] instanceof AlternativeNode))
                            tmpstates[k] = ((AlternativeNode)nodes[k]).getAccepting();
                        else
                            tmpstates[k] = istate.states[k];

                    TransitionPair current = ((TransitionPair[]) tmptrans
                            .get(j))[i];
                    tmpstates[stindex + 1 + j] = current.state;
                                      

                    trans[idx] = new TransitionPair(current.eventIndex,
                            new IndexState(stindex + 1 + j, tmpstates));
                }
            }

            return new TransitionPairs(trans);
        }

        else {
            TransitionPair[] atrans = nodes[stindex].getTransitions(istate.states[stindex]).transitions;
            int alen = atrans.length;

            TransitionPair[] trans = new TransitionPair[alen];
            for (int i = 0; i < alen; ++i) {
                State[] tmpstates = new State[istate.states.length];
                for (int k = 0; k < istate.states.length; ++k)
                    tmpstates[k] = istate.states[k];

                tmpstates[stindex] = atrans[i].state;

                trans[i] = new TransitionPair(atrans[i].eventIndex,
                        new IndexState(stindex, tmpstates));
            }

            return new TransitionPairs(trans);
        }
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getWeight()
     */
    public long getWeight() {
        if (weight != -1)
            return weight;
        else {
            weight = 0;
            for (int i = 0; i < nodes.length; ++i)
                weight += nodes[i].getWeight() - 1;

            return weight + 1;
        }
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#forwardCut(java.util.TreeSet)
     */
    public TreeNode forwardCut(TreeSet livingevents) {
        TreeNode active = null;
        int cnt = 0;

        for (int i = 0; i < nodes.length; ++i) {
            nodes[i] = nodes[i].forwardCut(livingevents);
            if (nodes[i] != null) {
                ++cnt;
                active = nodes[i];
            }
        }

        // no child node's survived
        if (cnt == 0)
            return null;

        // only one child node's survived and it hasn't been the only child
        // else we have to return the original node
        else if ((cnt == 1) && (nodes.length > 1))
            return active;

        // some of the child nodes have died
        else if (nodes.length != cnt) {
            TreeNode[] newchildren = new TreeNode[cnt];

            for (int i = 0, j = 0; i < cnt; ++i) {
                while (nodes[j] == null)
                    ++j;

                newchildren[i] = nodes[j++];
            }

            nodes = newchildren;
            last = nodes.length - 1;
        }

        return this;
    }

    /**
     * @return the symbolic name of the treenode denoting its type
     */
    public String[] getTypeName() {
        String[] result = { "Sequence", ";" };
        return result;
    }

    /**
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getAnotatedProtocol(org.objectweb.fractal.bpc.checker.state.State)
     */
    public AnotatedProtocol getAnotatedProtocol(State state) {
        IndexState istate = (IndexState) state;
        int nodecnt = nodes.length;
        String result = new String();
        ArrayList indicesresult = new ArrayList();

        for (int i = 0; i < nodecnt; ++i) {
            AnotatedProtocol subresult = nodes[i]
                    .getAnotatedProtocol(((istate != null) && (istate.index == i)) ? istate.states[i]
                            : null);

            for (int j = 0; j < subresult.indices.size(); ++j)
                indicesresult.add(new Integer(((Integer) subresult.indices
                        .get(j)).intValue()
                        + result.length()));

            result += subresult.protocol;

            if (i < nodecnt - 1)
                result += "; ";
        }

        return new AnotatedProtocol(result, indicesresult);
    }

    /**
     * This method is obsolete and used only for debuging, the protocol is
     * stored during the parse process
     * 
     * @return the protocol of this tree.
     */
    static private String getProtocol(TreeNode[] nodes) {
        String result = new String();
        result = "(" + nodes[0].protocol + ")";

        for (int i = 1; i < nodes.length; ++i) {
            result += "; (" + nodes[i].protocol + ")";
        }

        return result;

    }

    //--------------------------------------------------------------------------

    /**
     * Size of the node array
     */
    private int last;

    /**
     * cached initial state
     */
    private State initial = null;

}
